Nuprl Lemma : mon_when_thru_op 13,42

g:IMonoid, b:pq:|g|. (when b. (p * q)) = ((when bp) * (when bq))  |g
latex


Upgroups 1
Definitions of StatementIMonoid, when bp
Definitionsff, tt, t  T, if b then t else f fi , when bp, x:AB(x), x f y, P  Q, P & Q, P  Q, P  Q, Unit, , IMonoid,
Lemmasimon wf, bool wf, grp car wf, grp op wf, mon ident, grp id wf

origin